…ostulate

Step 2 of §3 (after the SafePath redesign in d7f07fb). normalizedIsSafe is now a
real proof, not an idris_crash:

    normalizedIsSafe p noDot = joinBySafe (normComponents p) (mkAllSafe p noDot)

- joinBy lifted to top level (renamed joinSep to avoid the Data.String.joinBy
  clash) and shared with normalizePath via normComponents, so normalizePath p
  reduces definitionally to joinSep "/" (normComponents p).
- joinBySafe builds SafePath of the join from per-component safety; SafeEmpty/
  SafeSingle/SafeComponent line up with joinSep's []/[x]/(x::y::ys) clauses.
- mkAllSafe derives, for each component: non-empty (filterSat), not ".." (else
  dotDotInfixOfJoin contradicts the premise), '/'-free (splitNoDelim + allFilter).
- ~13 supporting lemmas (filterSat, allFilter, allElem, allFromElem,
  appendEmptyLeft, joinByConsNonEmpty, the Bool/String micro-lemmas) are all
  total — they add nothing to the trusted base.

Trusted base grows by EXACTLY two fundamental opaque-String-primitive axioms:
  splitNoDelim      — split (== '/') yields '/'-free components
  dotDotInfixOfJoin — a ".." component is a ".." infix of the join
Both are genuine backend-semantics facts with no Idris2 reduction rules, in the
same justified category as the existing isPrefixOfBridge/unpackAppend bridges.

No believe_me / cast Refl / assert_total. cerro-torre.ipkg builds 7/7 green.
PROOF-NEEDS.md updated (17 partial sites; normalizedIsSafe -> PROVEN).

https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z

…laims

Reconcile the AffineScript/Ephapax threads as complementary roles, not
competitors, and align stale status docs with verified ground truth.

- Language policy (svalinn, cerro-torre, vordr component CLAUDE.md):
  AffineScript = primary general application language (ReScript replacement,
  typed-wasm); Ephapax = linear security core (exactly-once tokens, revocation,
  secret/handle lifecycle, container-lifecycle invariants, zero-copy IPC).
  Adds an Ephapax row to each ALLOWED-languages table.
- stapeln.toml: svalinn component description + language note now reflect the
  in-flight ReScript -> AffineScript (general) + Ephapax (linear core) migration
  (11/33 modules ported).
- ECOSYSTEM-STATUS.md: 2026-01-25 snapshot marked stale; selur ephapax/bridge.eph
  + types.eph are implemented (the "NOT EXISTS" line is obsolete).
- READINESS.adoc: Idris2 proofs are real (33 .idr, no believe_me/postulate),
  not "stubs only".

…tructor-link fix

The svalinn AffineScript migration blocker is NOT affinescript #138 (closed,
PR #193 — the resolver/typecheck half). The real blocker is an untracked
WASM-codegen gap: gen_imports never linked imported enum constructors, so
`use prelude::{Some, None}` consumers failed `compile` with
Codegen.UnboundVariable despite passing `check`. Implemented + verified the fix
locally against affinescript HEAD 58dc2a0 (458-test suite green incl. a new
WASM-target regression test; zero regressions on the conformance+modules corpus).

Persists the git-apply-able patch, a before/after repro script, and the
ready-to-file new-issue text so it survives container reclaim and a future
affinescript-scoped session can land it. Refs #96.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z

…mpiler + re-pin

SOURCE (container-stack/svalinn/src):
- Add explicit `use prelude::{Option, Some, None[, Result, Ok, Err]}` to the 6
  modules using those value constructors. They were ported against the old
  affinescript where Some/None/Ok/Err were seeded builtins; #138 (PR #193)
  removed that seed, so constructors must now resolve through the module path.
  AuthTypes + GatewayTypes now compile to WASM (4/11, was 2/11).
- Metrics: string concat `+` -> `++` (`+` is Int-only) and `let` -> `let mut`
  for reassigned locals. Now passes parse+typecheck; remaining blocker is the
  upstream WASM `float_to_string` builtin gap.

TOOLCHAIN (re-pin):
- Bump AFFINESCRIPT_REF d2875a5 (does not build — menhir r/r conflict) ->
  58dc2a0 (current HEAD, verified building) in the workflow, Containerfile, and
  migration task doc.
- Carry the vetted WASM cross-module constructor-linking patch (merged in #105)
  in the build until it lands upstream in affinescript; then drop the apply and
  bump the pin to the merged SHA.

Verified locally (affinescript 58dc2a0 + the patch): 4/11 modules compile to
WASM. Remaining blockers: 4 parse errors (Main/Json/PolicyEngine/Client —
unsupported syntax), 2 sibling-module resolutions (Authz/SecurityHeaders —
single-file compile has no src/** search path), 1 upstream WASM builtin gap
(Metrics float_to_string). Refs #96.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z

…jan-2uoae

…fe5a)

The `governance / Check Workflow Staleness` gate flagged the governance, Hypatia,
and Scorecard reusable workflows as pinned to a pre-cache/baseline-fix standards
SHA — which is why `scan / Hypatia Neurosymbolic Analysis` died at "Prepare all
required actions" (unresolvable actions/cache@d4373f26… inside the old reusable).
hyperpolymath/standards already fixed it upstream; bump the three flagged pins to
current standards HEAD d72fe5a. (scorecard-enforcer.yml was already removed on
main.) Fixes the estate-wide Hypatia + workflow-staleness CI failures.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z

…jan-2uoae